\chapter{相关工作综述}
\label{cha:related}
本章对网络可靠性和适应性相关的前沿研究工作进行了综述。首先介绍了网络验证领域的最新研究进展，主要包括控制平面验证和数据平面验证。随后，本章探讨了致力于提高网络适应性的网络协同应用编程的最新技术。通过对相关工作的全面总结，提出了已有工作在现代网络背景下的主要问题和限制，为后续章节的研究工作提供了重要背景和动机。

% 本章主要对网络与应用协同编程和数据平面验证相关工作进行综述，从多个维度对相关工作进行归纳总结。同时探讨现有工作存在的主要问题。

% 现代SDN网络架构一般分为控制平面和数据平面，与之相应的网络验证技术也主要分为控制平面验证和数据平面验证。其中数据平面实现具体的数据包转发，而控制平面负责提供南北向接口,其中南向接口对数据平面进行配置，从而实现相应的数据包转发策略，北向接口实现网络编程和管理的API。



\section{网络验证相关工作}
在提高网络可靠性方面，国内外已经开展了广泛的研究。在该领域，网络验证已经成为保障网络可靠性的主要技术手段之一。对于网络验证系统的系统架构，研究者们提出了许多设计方案，主要可以分为两个主要方向，即控制平面验证（Control Plane Verification, CPV）和数据平面验证（Data Plane Verification, DPV）。这两个方向致力于解决网络验证过程中的不同关键问题，以确保网络的正确性。控制平面验证主要关注网络的控制平面逻辑和协议的正确性，而数据平面验证则主要关注网络数据包在数据平面中的真实传输过程的正确性。这两个方向的研究共同推动着网络可靠性的提高，为网络的可靠性保障提供了坚实的基础。

% 相应的架构也包括集中式设计和分布式设计。如\cref{fig:schemes}所示，集中式架构依赖于服务器来收集网络中设备的FIB（Forwarding information base）。
% 集中式设计的一个主要问题是它可能面临可靠性和可伸缩性问题。例如，如果服务器崩溃或与网络的一部分断开连接，则检测系统变得不可用。现有工作中主要有两种类型的分布式方法，一种是通过拓扑划分方式来实现分布式，其中每个服务器负责网络中的设备子集[5]。另一个由数据包头空间划分实现分布式，其中每个服务器负责标头空间的子集。这些分布式方案采用服务器集群来增强验证系统的可扩展性，并在如Libra[6]等系统中实现毫秒级验证时间。然而，从设备获取FIB更新的延迟并不可忽略，根据RCDC[4]的研究,从设备获取每个路由表需要200-800毫秒。在实践中，出于安全或自适应的原因，验证系统通过管理网络获取设备的FIB，然而，管理网络通常具有低带宽、长延迟并且需要根据需求进行按需配置，这给基于服务器的验证方法带来了效率和可用性问题。


% 为了进一步提高验证系统的性能和可扩展性，我们提出了一种基于网内计算的分布式方案。在该方案中，我们将网络设备视为集群，设备的FIB在集群中形成分布式数据集。每个设备都运行一个轻量级代理进程，代理有效地监控本地FIB更新，并在FIB更改时采取相应动作。验证任务直接分配给代理，代理使用高速数据路径相互通信，如图~\ref{fig:schemes}的最后一张图所示。

% \begin{figure}[htbp]
%   \centering
% \includegraphics[width=\textwidth]{schemes.pdf}
%   \caption{数据平面验证主要架构}
%   \label{fig:schemes}
% \end{figure}

% 集中式数据平面验证通过一台服务器收集网络的数据平面信息，通过构建有利于实施验证算法的数据平面模型（如SAT，等价转发类），然后在模型上实施相应的验证算法（如SAT求解，图遍历）实现数据平面验证。

\subsection{控制平面验证相关工作}
网络控制平面验证是通过分析控制平面配置来验证网络的正确性，\cref{fig:related-cpv}所示为控制平面验证的主要架构。控制平面验证的过程首先涵盖网络相关配置的收集，其中包括拓扑和设备设置、BGP（Border Gateway Protocol）配置，以及IGP（Interior Gateway Protocol）配置等。控制平面验证系统会对这些配置进行详细的分析和建模，其方法主要包括语法验证、静态分析、SMT（Satisfiability Modulo Theories）建模以及数据平面模拟。通过这些手段，系统能够有效地进行网络验证，从而检测配置文件中的语法错误、无效配置，以及涉及路由的可达性、路由环路和路由黑洞等问题。\cref{tab:related-cpv}列出了当前主要的控制平面验证相关工作。

\begin{figure}[htbp]
  \centering
  \includegraphics[width=0.9\textwidth]{figures/related/cpv.pdf}
  \caption{控制平面验证主要架构}
  \label{fig:related-cpv}
\end{figure}

\textbf{基于静态分析的控制平面验证。}
基于静态分析的控制平面验证通过对控制平面配置进行静态分析从而发现网络错误。rcc~\cite{feamster2005detecting} 是首个具备自动检测真实网络中 BGP 配置错误能力的静态分析工具。rcc 对BGP配置文件进行解析从而实现了综合且统一的配置表示方式。在 BGP 领域，定义高级的正确性规范是相当困难的，而且这些规范必须适应实际配置来进行测试。rcc 在这一问题上取得了显著的突破，rcc可以检测两类广泛的故障：路由有效性故障和路径可见性故障。路由的有效性要求路由器正确传播现有的可用 IP（Internet Protocol）层路由。路径的可见性则表示路由器能够学习到网络中存在的路径对应的路由。rcc 使用这些规范来推导出约束，使用户能够检测到整个网络配置中的错误，从而有助于改善互联网的路由基础设施。

\textbf{基于数据平面生成的控制平面验证。}
基于数据平面生成的控制平面验证通过收集控制平面配置（如BGP、IGP和拓扑）并推导生成数据平面配置来进行验证。如Batfish~\cite{fogel2015general}通过以下四个步骤来验证控制平面配置。首先，它以网络配置文件为输入，然后将这些输入编码为一组逻辑事实。接下来，它在LogiQL~\cite{huang2011datalog}中生成逻辑控制平面模型，并通过模拟协议工作方式生成数据平面。然后，Batfish使用NoD~\cite{lopes2015checking}执行数据平面分析。最后，它通过数据平面模型模拟反例数据包的行为，以帮助操作员理解网络错误并修复网络配置。Batfish最大的问题在于数据平面配置生成过程效率低下，使用Batfish对一个简单的配置文件进行验证需要将近两个小时，FastPlane~\cite{lopes2019fast}则基于BGP优先级在传播过程中的单调性特征，提出了比Batfish快两个数量级的数据平面生成方法，然而，FastPlane只能针对BGP协议生成数据平面。RealConfig~\cite{zhang2020incremental}基于Batfish生成数据平面配置，并通过Datalog表示控制平面的增量更新。然而，基于数据平面生成的控制平面验证需要消耗大量时间生成数据平面配置，在大规模网络情况下导致整体系统效率低下。



\begin{table}[htbp]
  \center
  \caption{控制平面验证相关工作}
  \label{tab:related-cpv}
  % \resizebox{\linewidth}{!}{
  \begin{tabular}{|m{2.3cm}|m{2.3cm}|m{4cm}|m{4cm}|}
    \hline
    \emph{研究工作}
    & \emph{基于技术}
    & \emph{验证方法}
    & \emph{主要问题}
    \\\hline
    rcc~\cite{feamster2005detecting} & 静态分析 & BGP配置分析 & 仅适用于特定BGP协议
    \\\hline
    Batfish~\cite{fogel2015general} & 数据平面生成 & 基于控制平面配置生成数据平面配置，利用NoD执行验证 & 数据平面配置生成效率低下，路由规则直接作为Datalog数据导致验证速度较慢
    \\\hline
    ARC~\cite{gember-jacobson2016fast} & 数据平面模拟 & 图计算 & 仅对部分协议进行建模，通用性和扩展性不足
    \\\hline
    ERA~\cite{fayaz2016efficient} & BDD & 使用BDD表示控制平面路由公告分发过程 & 无法检测收敛过程中的网络错误
    \\\hline
    Minesweeper~\cite{fogel2015general} & SMT & STM求解 & 对于大规模网络需要大量的SMT约束，伸缩性不足
    \\\hline
    NICE~\cite{canini2012nice} & 程序分析 / 符号执行 & 通过符号执行分析Openflow控制平面程序 & 仅适用于特定语言编写的Openflow程序，且存在状态爆炸问题
    \\\hline
    DeLorean~\cite{croft2015systematically} & 程序分析 / 时序自动机 & 将控制程序的时序映射到网络状态以解决状态爆炸问题 & 控制程序的复杂性导致其时序难以获取
    \\\hline
    Plankton~\cite{prabhu2017predicting} & 模型检测 / 自动机 & 对控制平面收敛过程进行建模 & 大规模网络状态爆炸
    \\\hline
    Bonsai~\cite{beckett2018control} & \multirow{3}{2cm}{代数抽象} & \multirow{3}{4cm}{对控制平面配置进行代数建模，压缩为更小的等价控制平面代数模型} & \multirow{3}{4cm}{只适用于特定标准路由协议，扩展性较差}
    \\\cline{1-1}
    ShapeShifter~\cite{beckett2019abstract} &  &  &
    \\\cline{1-1}
    Origami~\cite{giannarakis2019efficient} &  &  & 
    \\\hline
    FastPlane~\cite{lopes2019fast} & 数据平面生成 & 基于BGP优先级在传播过程中的单调性特征生成数据平面 & 仅支持BGP协议
    \\\hline
    Tiramisu~\cite{abhashkumar2020tiramisu} & 数据平面模拟 & 基于分层图结构模拟网络行为 & 无法验证控制平面收敛过程中的错误
    \\\hline
    Hoyan~\cite{ye2020accuracy} & SMT & SMT求解 & 大规模网络下大量SMT约束导致较差的伸缩性
    \\\hline
    NUV~\cite{li2020assisting} & 代数抽象 & 对控制平面更新进行代数抽象 & 仅支持特定控制平面协议
    \\\hline
    RealConfig~\cite{zhang2020incremental} & 数据平面生成 & 基于Datalog实现控制平面增量验证 & 基于Batfish生成数据平面效率低下
    \\\hline
    DNA~\cite{zhang2022differential} & 原子谓词 & 图计算 & 基于APKeep的单次更新验证过程无法应对大规模网络
    \\\hline
  \end{tabular}
  % }
\end{table}

\textbf{基于数据平面模拟的控制平面验证。}
基于数据平面模拟的控制平面验证通过收集控制平面配置并推导生成数据平面对应的转发图模型来进行验证。相比基于数据平面生成的控制平面验证，基于数据平面模拟的控制平面验证能够提高验证的效率。ARC~\cite{gember-jacobson2016fast}通过控制平面配置构建数据平面的连通图模型，网络验证被抽象为简单的图连通性验证，由于ARC并不生成实际的数据平面配置，ARC的速度相比Batfish快了一个数量级。然而，ARC只支持特定的路由协议，Tiramisu~\cite{abhashkumar2019tiramisu}则通过多层图抽象以扩展表达更多的协议。然而，基于数据平面模拟的控制平面验证跳过了控制平面的收敛过程，导致不完整的验证结果。

\textbf{基于模型检测的控制平面验证。}
基于模型检测的控制平面验证对控制平面的执行过程和状态进行建模，从而能够发现控制平面收敛过程中的错误。如Plankton~\cite{prabhu2017predicting}利用模型检测技术对控制平面可能的收敛过程进行分析。然而，基于模型检测的控制平面验证在小规模网络下有效，在大规模网络情况下存在显著的状态爆炸问题。

\textbf{基于代数抽象的控制平面验证。}
基于代数抽象的控制平面验证将控制平面行为进行代数抽象，从而能够以简洁的代数方式表达复杂的控制平面行为。如Bonsai~\cite{beckett2018control}基于SRP（Stable routing problem）将控制平面建模为一系列代数关系，从而得到易于分析且更精简的等价代数表达。然而，Bonsai的代数系统无法表达网络中的多链路情况，Origami~\cite{giannarakis2019efficient}对此问题进行了改进，且支持多链路失效分析。ShapeShifter~\cite{beckett2019abstract}则进一步对路由协议进行压缩，牺牲了验证的可靠性以提高验证效率，其效率相比Batfish提高2个数量级。NUV~\cite{li2020assisting}进一步对控制平面更新进行了代数抽象，从而能够验证控制平面更新带来的差异。然而，基于代数抽象的控制平面验证只能针对有限的标准路由协议进行建模，其扩展性较差。

% \textbf{基于Datalog的控制平面验证}
% 现有的配置分析工具如rcc只为特定协议开发了定制的模型。因此，可以检查的范围有限。Batfish [94]克服了这一挑战。它通过四个步骤验证控制平面配置。首先，它将网络配置文件作为输入；然后，将输入编码为一组逻辑事实。接下来，它使用LogiQL [37]生成逻辑控制平面模型。通过环境（每个链接状态和路由公告），它执行LogiQL程序。Batfish可以获得数据平面模型。第三步使用户能够检查数据平面模型。Batfish使用NoD [65]进行数据平面分析。最后，它通过数据平面模型模拟反例数据包的行为。这一步可以帮助运营商了解属性违规情况并修复网络配置。然而，Batfish在大规模网络以及实时验证情况下不适用，使用Batfish [94]对一个简单的配置文件进行验证需要将近两个小时，因为它需要模拟网络链路的数量与生成数据平面时一样多。换句话说，Batfish [94]在将配置文件转换为数据平面转发逻辑的过程中花费了大量时间。然而，它的输入仍然是实际拓扑环境的子集。


\textbf{基于BDD的控制平面验证。}
基于BDD的控制平面验证通过BDD（二叉决策图）~\cite{akers1978binary}来紧凑地表示控制平面的路由公告。具体而言，BDD结构能够很好地解决控制平面验证面临的两个挑战：表达能力（如路由网络协议的多样行为）和可扩展性（对网络信息进行建模）。为了解决这些挑战，ERA~\cite{fayaz2016efficient}构建了网络控制平面的模型，并使用一系列技术来进行可扩展的模型分析。ERA首先设计了一个统一的抽象表示，即路由（route），它简明地捕捉了各种协议及其交互的多样行为。通过将路由器抽象为函数为其邻居生成路由公告，然后ERA使用BDD来紧凑地表示路由公告，并使用公告的等价类来优化表示，ERA还使用一些技术如K-map~\cite{hill1981introduction}进一步优化其数据结构。因此，对于具有一千多个路由器的网络，仅需几秒钟即可识别出各种策略中可转化为可达性关系的错误。然而，ERA无法检测到瞬态状态或收敛错误中的可达性错误。

\textbf{基于SMT的控制平面验证。}
基于SMT的控制平面验证将控制平面配置建模为SMT约束问题，通过求解SMT问题实现网络验证。如Minesweeper~\cite{fogel2015general}基于SMT的模型将数据平面配置建模为一系列约束条件，它适用于大量的网络协议、特性和拓扑结构，并且可以验证所有从控制平面产生的数据平面的大量属性。它使用基于图的模型，其中边和节点上的SMT逻辑约束编码了所有可能的路由消息交互。它将网络的稳定状态编码为对SMT公式的满足赋值。Hoyan~\cite{ye2020accuracy}通过分析不同厂商控制平面配置的差异，利用SMT对控制平面进行建模，以提高控制平面验证的适应性。然而，基于SMT的控制平面验证在大规模网络情况下会产生大量的SMT约束，导致较差的伸缩性。

\textbf{基于程序分析的控制平面验证。}
基于程序分析的控制平面验证主要通过分析控制平面程序的正确性来验证SDN网络。如 NICE~\cite{canini2012nice} 主要针对OpenFlow应用程序进行测试。它创建了虚拟网络拓扑，部署OpenFlow应用，设计了多种测试场景，模拟不同的网络情景，并通过性能分析来评估应用在这些情景下的表现。然而，在面对大规模网络或复杂的控制程序时可能会遇到状态空间爆炸的挑战。DeLorean~\cite{croft2015systematically}则使用时序自动机（Timed automata, TA）~\cite{alur1994theory}来建模SDN程序，从而避免状态爆炸问题，然而，虚拟化环境可能与实际网络环境不完全一致，比如真实网络的链路可能随时发生故障，因此测试结果在某些情况下可能无法完全反映真实网络中潜在的问题。

% \textbf{主要问题。}
% \begin{enumerate}
%   \item 无法检测收敛过程中的网络错误
% \end{enumerate}


\subsection{数据平面验证相关工作}
\begin{figure}[htbp]
  \centering
  \includegraphics[width=0.9\textwidth]{figures/related/dpv.pdf}
  \caption{数据平面验证主要架构}
  \label{fig:related-dpv}
\end{figure}

网络数据平面验证是通过分析数据平面配置以验证网络的正确性。\cref{fig:related-dpv}显示了数据平面验证的主要架构。该过程首先涵盖了数据平面相关配置的收集，包括FIB（Forwarding Information Base）和拓扑信息。数据平面验证系统会对这些配置进行详细的分析和建模，主要采用符号执行、转发等价类、原子谓词、SAT/SMT以及Datalog等方法。通过这些手段，系统能够高效地进行网络验证，检测数据平面的无效规则，以及涉及路由的路径可达性、路由环路和路由黑洞等问题。\cref{tab:related-dpv}列出了当前主要的数据平面验证相关工作，本节按照其主要采用的验证方法对这些工作进行分析。


\begin{table}[]
  \center
  \caption{数据平面验证相关工作}
  \label{tab:related-dpv}
  % \resizebox{\linewidth}{!}{
  \begin{tabular}{|m{2.3cm}|m{2cm}|m{4cm}|m{4cm}|}
    \hline
    \emph{研究工作}
    & \emph{基于技术}
    & \emph{验证方法}
    & \emph{主要问题}
    \\\hline
    ConfigChcker~\cite{al-shaer2009network} & \multirow{2}{3cm}{模型检测} & 数据平面抽象为状态机，数据包状态用BDD编码 & \multirow{2}{4cm}{大规模网络情况下状态爆炸}
    \\\cline{1-1}\cline{3-3}
    FlowChcker~\cite{al-shaer2010flowchecker} &  & 基于ConfigChecker实现SDN网络验证 & 
    \\\hline
    Anteater~\cite{mai2011debugging} & \multirow{2}{4cm}{SAT} & \multirow{2}{4cm}{SAT求解} & \multirow{2}{4cm}{大规模网络下变量数量和约束条件数量爆炸}
    \\\cline{1-1}
    NetSAT~\cite{zhang2013sat} &  &  & 
    \\\hline
    HSA~\cite{kazemian2012header} & 符号执行 & 数据平面行为模拟 & \multirow{2}{4cm}{直接用比特串表示的转发规则导致较差的性能}
    \\\cline{1-3}
    NetPlumber~\cite{kazemian2013real} & 符号执行 & 数据平面行为模拟/实时数据平面模型更新 & 
    \\\hline
    Veriflow~\cite{khurshid2012veriflow} & 转发等价类 & 图算法 & 基于Trie tree结构表示的路由规则计算等价类计算过程复杂
    \\\hline
    NOD~\cite{lopes2015checking} & Datalog & Datalog分析 & 比特串作为Datalog数据导致验证速度较慢
    \\\hline
    SymNet~\cite{stoenescu2016symnet} & 符号执行 & 数据平面行为模拟/ middlebox建模为函数 & 仅支持特定的middleboxes
    \\\hline
    APV~\cite{yang2016realtime} & \multirow{4}{2cm}{Atomic predicates} & \multirow{4}{2cm}{图算法} & \multirow{2}{4cm}{增量更新导致重新计算全局AP}
    \\\cline{1-1}
    APT~\cite{yang2017scalable} &  &  & 
    \\\cline{1-1}\cline{4-4}
    APC~\cite{wang2015practical} &  &  & \multirow{2}{4cm}{关注单个更新的处理，大规模网络下性能不佳}
    \\\cline{1-1}
    APKeep~\cite{zhang2020apkeep} &  &  & 
    \\\cline{1-2}\cline{3-3}\cline{4-4}
    DeltaNet~\cite{horn2017deltanet} & Atom & 图算法 & 无法有效表示非前缀规则
    \\\hline
    ddNF~\cite{bjorner2016ddnf} & \multirow{2}{2cm}{ddNF表示转发等价类} & 利用三元位向量(Ternary bit-vectors, TBV)表示包头空间 & 无法判断等价类为空集
    \\\cline{1-1}\cline{3-4}
    \#PEC~\cite{horn2019precise} &  & 基于ddNF计算转发等价类 & 不支持增量式更新
    \\\hline
    SRE~\cite{zhang2022symbolic} & 符号执行 & 通过符号执行计算包失败等价类（PFEC） & 不支持增量式更新
    \\\hline
    Libra~\cite{zeng2014libra} & 分布式计算 & 通过子网划分包头空间，利用MapReduce框架验证 & 在无明确子网划分规则的网络中难以实施 
    \\\hline
    RCDC~\cite{jayaraman2019validating} & 分布式计算 & 对网络设备进行划分 & 只适用于特定数据中心网络和路由协议
    \\\hline
  \end{tabular}
  % }
\end{table}

\textbf{基于状态机的数据平面验证。}基于状态机的数据平面验证通过状态机构建数据平面转发模型。ConfigChecker~\cite{al-shaer2009network}将数据平面行为抽象为有限状态自动机（Deterministic Finite Automaton, DFA），同时用BDD（Binary Decision Diagram, BDD）表示数据包状态，端到端的验证结果通过计算BDD表达式的值获得。FlowChecker~\cite{al-shaer2010flowchecker}则基于ConfigChecker进一步实现了对SDN网络数据平面的验证。然而，基于状态机的数据平面验证在大规模网络情况下会有状态爆炸问题。

\textbf{基于SAT的数据平面验证。}
基于SAT的数据平面验证技术将数据平面的需求（如可达性）建模为可满足性问题，如Anteater~\cite{mai2011debugging}是第一个用SAT Solver检测网络错误的数据平面验证系统。首先，它通过收集网络设备中的转发表获得数据平面快照。其次，用户定义对应网络策略的不变量（例如，可达性）。第三，它将快照编码为布尔表达式，并将不变量转换为SAT目标。然后，Anteater使用SAT Solver检查不变量的可满足性。系统求解SAT问题时可以输出反例信息（例如，数据包头和相应的FIB条目），以在发现违规配置时帮助诊断错误。

NetSAT~\cite{zhang2013sat}是将数据平面验证问题简化为SAT问题的另一种方法。NetSAT还提供了一个网络建模框架，可以同时验证多个网络不变量。与Anteater相比，它获得了更好的性能。比如，在Anteater中，检测网络循环是通过对每个设备生成两个副本，并检查每个设备是否可以到达其副本。每个设备必须单独检查，从而效率低下。相反，NetSAT将网络与不变公式分开，然后通过构建一个公式并检查循环不变量，所以NetSAT更加模块化，消除了SAT求解过程中的冗余计算。

然而，Anteater和NetSAT都有局限性。首先，如果FIB在收集过程中动态变化，将生成不一致的数据平面快照，从而导致误报。第二，如果网络遭受可达性故障，则很难收集FIB快照。第三，这些系统具有较差的可扩展性和效率。例如，Anteater需要两个小时检查校园网络中的三个标准不变量。此外，这些系统仅在发生不变违规时提供一个反例，这使得很难找到导致违规的所有相关FIB条目。

\textbf{基于符号执行的数据平面验证。}
基于符号执行的数据平面验证将传统符号执行技术应用到数据平面验证系统中，如Kazemian等人提出的HSA~\cite{kazemian2012header}通过符号执行来模拟数据平面行为。HSA将网络设备（例如路由器和防火墙）抽象为包头集上的传输函数，通过沿所有路径来计算任意两个节点的可达性集合实现验证过程。它可以用几种算法检查网络不变量（例如可达性故障、路由循环和切片隔离）。然而，由于HSA基于OpenFlow规则结构作为表达包头空间的符号，使得其遍历网络时的计算效率低下。SymNet~\cite{stoenescu2016symnet}将网络和middleboxes建模为行为函数，包头作为符号，通过符号执行验证数据平面是否满足预期行为，但SymNet仅支持部分特定的middleboxes。而SRE~\cite{zhang2022symbolic}实现了一个更通用的、可扩展的网络验证引擎，它支持不同类型的分析。SRE符号化地运行网络模型来发现数据包失效等价类（Packet failure equivalence classes, PFECs） 。通过用BDD符号化数据包头和故障，SRE允许操作人员用基于BDD的图算法分析属性。基于符号执行的数据平面验证能够很好地表达包头语义，但是对于复杂的数据平面规则缺乏统一的表示。

\textbf{基于Datalog的数据平面验证。}
基于Datalog的数据平面验证将数据平面配置表示为Datalog，验证过程通过Datalog查询实现。如NoD~\cite{lopes2015checking}利用Datalog实现了多种包头协议表示和网络属性查询。然而，基于Datalog的数据平面验证对Datalog的处理相对复杂，所以验证效率不高。

\textbf{基于转发等价类的数据平面验证。}
基于转发等价类的数据平面验证将具有相同转发行为的包头空间合并为一个等价类。如Veriflow~\cite{khurshid2012veriflow}将包头空间划分为转发等价类（Forwarding Equivalence Classes, FEC），每个等价类的包头在整个网络中有相同的转发动作。其次，它为每个EC构建单独的转发图，然后通过图计算算法实现验证。当网络发生变化（例如，插入了转发规则）时，只需要对受影响的EC进行增量式验证。ddNF~\cite{bjorner2016ddnf}提出了新的数据结构来表示包头空间，然而ddNF结构无法判断等价类为空的情况，进而导致错误的验证结果。\#PEC~\cite{horn2019precise}基于ddNF实现了等价类的计算，并修复了ddNF存在的判断空集错误，然而\#PEC不支持增量式的等价类计算。基于转发等价类的数据平面验证定义了非常紧凑的数据平面等价模型，然而需要一种更有效的数据结构来表示等价类并支持高效的增量式更新。

\textbf{基于原子谓词的数据平面验证。}
基于原子谓词的数据平面验证利用谓词（Predicate）表示包头空间。APV~\cite{yang2016realtime}比以前的网络验证工具（如NetPlumber和Veriflow）更有效，它将数据包过滤器表示为一组原子谓词（Atomic Predicates, AP）。APV开发了一种AP的算法，每个谓词都可以表示为原子谓词的析取，另外，APV使用BDD对谓词进行编码，并使用整数索引AP，谓词的析取和合取操作计算变为了整数集的并集和交集操作，因此，包头操作可以实现快速计算。然而，在增量式数据平面更新情况下，APV采用重复计算全局AP，导致其性能不佳。为了解决增量式更新问题，APC~\cite{wang2015practical}基于二叉树结构实现了AP的增量式计算。APKeep~\cite{zhang2020apkeep}则通过split-transfer-merge三个过程实现了增量式AP计算，当网络数据平面发生更新时，能够实现微秒级的增量式验证。然而，当前基于原子谓词的数据平面验证工作关注于单个规则更新的效率，对于大规模网络下的大量更新处理性能不佳，相关工作在Facebook数据中心规模的网络上验证时间超过10小时。

\textbf{基于原子区间的数据平面验证。}
基于原子区间的数据平面验证利用整数区间表示包头空间。如DeltaNet~\cite{horn2017deltanet}采用一种基于整数区间（atom）的方式表示数据包头空间，在只有前缀匹配规则的情况下相对高效。然而，该方法在存在非前缀规则情况下（如任意位置存在wildcard匹配）会产生大量的atom，导致数据包头计算效率低下。


\textbf{分布式数据平面验证。}
虽然集中式数据平面验证（如Anteater，Veriflow和APKeep等工具）可以较为快速地发现网络错误，但它们无法扩展到大型数据中心。在数据中心网络中，转发状态的变化使得验证系统难以获得准确的快照（例如，不同的路由过程使用不同步的时钟更新其交换机状态）。不准确的数据平面快照可能导致误报。为了应对这些挑战，已有工作通过对数据平面配置进行划分从而实现分布式数据平面验证，主要包括基于包头空间划分的分布式数据平面验证和基于设备划分的分布式数据平面验证。如Libra~\cite{zeng2014libra}通过对包头空间按照子网进行划分，从而实现一种新的验证大型网络的分布式方法。一方面，Libra记录来自路由过程的网络事件流，并提供一种算法来捕获大规模网络中的流表和一致数据平面快照。另一方面，它对包头空间进行划分，利用MapReduce模型并行地对各个子空间进行验证，从而大大提高了验证效率。而RCDC~\cite{jayaraman2019validating}通过将数据中心的网络设备进行划分，并利用服务器集群进行数据平面验证，集群中的每个服务器负责网络中一部分设备的验证，然而，由于服务器和网络设备之间的通信延迟，使得获取设备FIB需要O(200-800ms)的时间规模，这限制了整个验证系统的实时性。



\section{网络协同应用编程相关工作}

\begin{figure}[htbp]
  \centering
  \includegraphics[width=0.9\textwidth]{figures/related/aan.pdf}
  \caption{应用感知网络主要架构}
  \label{fig:related-aan}
\end{figure}

为了实现网络的高适应性需求，近年来，如何将应用程序和网络整合起来已经得到了广泛的研究，网络协同应用（Networking-application Integration，NAI）技术是实现该目标的主要方法之一。具体而言，网络与应用协同主要可分为应用感知网络（Application-aware Networking, AAN）、网络感知应用（Networking-aware Application, NAA）以及网络和应用双向感知（Networking-application Bidirectional Awareness, NABA）三个方向。

% 已有工作目前主要通过两种方式来解决应用程序和网络之间的交互。许多分布式应用程序需要网络提供一组标准API~\cite{gallo2014nanet}。它们通过API与网络交互，并且简单地在每个端点上进行编程，而不考虑特定的网络细节。网络编程是由网络操作员分开处理的。然而，操作员可能对端点的要求一无所知，不能为不同的用户需求设计一个全局最优设计。另一组尝试直接将网络设计融入应用程序中。随着新兴的可编程网络显示出处理某些应用程序逻辑的巨大潜力，许多研究~\cite{tokusashi2019case, jin2018netchain,jin2017netcache} 提出将一些应用程序逻辑移至网络中，利用网络的位置中心性~\cite{jin2018netchain} 并节省路径延迟~\cite{jin2017netcache}。然而，这种端到端和网络之间的统一描述仅限于特定的应用程序上下文中。在一个系统中动态支持不同的应用程序仍然是一个正在进行中的问题。此外，它们只是在端点和交换机之间分配角色，并在每个实体上进行编程。


\subsection{应用感知网络相关工作}

\begin{table}[htbp]
  \center
  \caption{应用感知网络相关工作}
  \label{tab:related-nai-aan}
  \begin{tabular}{|m{2.1cm}|m{1.8cm}|m{4.5cm}|m{4.5cm}|}
    \hline
    \emph{研究工作}
    & \emph{协同类型}
    & \emph{协同方式}
    & \emph{主要问题}
    \\\hline
    RSVP~\cite{braden1997resource} & In-band & 资源预留 & 为每个流维护上下文，会导致伸缩性问题，资源预留导致网络利用率下降
    \\\hline
    DiffServ~\cite{nichols1998rfc2474} & In-band & 区分服务代码点(DSCP) & 对流量控制的粒度较大，导致不必要的数据包被标记为高优先级
    \\\hline
    Socket Intents~\cite{schmidt2013socket} & Out-band & 应用需求与物理端口绑定 & 以物理端口区分的网络QoS无法实现细粒度的网络控制
    \\\hline
    Google SDN WAN~\cite{yap2017taking} & Out-band & 边缘网络控制器收集应用状态 & 只适用于特定网络和协议
    \\\hline
    CAMARA~\cite{ordonez-lucena2022pathways} & Programming & 应用程序集成QoD(Quality-on-Demand)API & 对单套接字多数据流应用无法提供细粒度的网络控制
    \\\hline
    EdgePeering~\cite{wang2022lowlatency} & Out-band  & 网络的边缘设备协同控制路由 & 需要额外的链路和协议构建边缘节点的信息交互通道
    \\\hline
    EarlyBird~\cite{mortazavi2022earlybird} & Out-band & 在终端设备获取应用程序历史状态预测网络需求 & \multirow{2}{4.5cm}{对于运行时间较短的应用无法提供准确结果}
    \\\cline{1-3}
    QoS-KPI~\cite{jahromi2018applicationaware} & Out-band & 通过控制器收集应用需求 & 
    \\\hline
  \end{tabular}
\end{table}

应用感知网络（Application-aware Networking, AAN）旨在通过让网络获取应用信息从而调整网络逻辑，主要通过收集和监测应用程序的需求和行为，对网络配置进行调整和优化。这包括流量工程、负载均衡、带宽分配等技术，以提供更好的网络服务质量（QoS）和用户体验。\cref{fig:related-aan}所示为网络感知引用的主要架构，系统通过收集应用的需求，如视频流应用需要高带宽，实时消息应用需要低时延以及文件传输应用需要低丢包率等需求，对这些需求进行综合分析，并调整网络配置以满足不同应用的不同需求。

\textbf{基于带内（In-band）控制的应用感知网络。}基于带内控制的应用感知网络利用与数据传输相同的路径获取应用需求并控制网络。如RSVP~\cite{braden1997resource}是一个基于IP协议的网络资源预留协议，用于在数据流所经路径上为该流进行资源预留，从而满足该流的QoS要求。然而，RSVP存在两个问题：1）如果为每个流维护上下文，会导致伸缩性（Scalability）问题；2）这种资源保留方法可能降低网络资源的整理利用率。另一种网络端的方法是网络为不同的流量类型提供不同的优先级，例如，在DiffServ~\cite{nichols1998rfc2474}QoS模型中使用的区分服务代码点（Differentiated Services Code Point, DSCP）。使用DSCP可以更简单地实现并具有更好的可扩展性，而不需要为每个IP流在路由器中维护上下文。然而，DiffServ对流量控制的粒度较大，应用程序可能会将不必要的数据包标记为较高的优先级。

\textbf{基于带外（Out-band）控制的应用感知网络。}基于带外控制的应用感知网络通过与数据传输不同的路径获取应用需求并控制网络。如Socket Intents~\cite{schmidt2013socket} 扩展了套接字接口以表达应用程序的需求，Socket Intents系统的核心思想是利用应用程序对网络连接的意图进行描述和传达。通过与应用程序的交互，系统可以获取应用程序对网络连接的需求和优先级。根据这些信息，系统可以动态地选择最合适的网络连接，并实施相应的策略，
% 如连接切换、带宽分配和连接保持等，以优化应用程序的性能和用户体验，
然而，Socket Intents以物理端口区分的网络QoS无法实现细粒度的网络控制。Google的SDN WAN~\cite{jain2013b4}和边缘网络~\cite{yap2017taking} 使用本地控制器收集应用程序状态，并将其交给中央控制器决定流量分配，但该系统只适用于特定网络和协议。EdgePeering~\cite{wang2022lowlatency}通过网络的边缘设备协同控制路由，但需要额外的链路和协议构建边缘节点的信息交互通道。EarlyBird~\cite{mortazavi2022earlybird}通过在终端设备上收集应用程序历史状态进而预测网络需求，QoS-KPI~\cite{jahromi2018applicationaware}通过SDN控制器收集应用状态，但它们对于运行时间较短的应用无法提供准确结果。

\textbf{基于协同编程（Programming）的应用感知网络。}基于协同编程的应用感知网络在编程角度通过相应的API实现网络对应用的感知。如CAMARA~\cite{ordonez-lucena2022pathways}通过QoD（Quality-on-Demand）API实现程序向网络提交其需求（如带宽和延时）功能。然而它对单套接字多数据流（Single Socket Multiple Data Stream, SSMD）应用无法提供细粒度的网络控制。

\subsection{网络感知应用相关工作}

\begin{figure}[]
  \centering
  \includegraphics[width=0.95\textwidth]{figures/related/naa.pdf}
  \caption{网络感知应用主要架构}
  \label{fig:related-naa}
\end{figure}

网络感知应用（Networking-aware Application, NAA）主要使应用程序结合网络状态来提高应用性能。\cref{fig:related-naa}所示为网络感知应用的主要架构，系统通过收集网络的状态信息，如路径带宽、路径延时以及丢包率等信息，应用程序结合这些信息可以调整其数据压缩率、调整TCP缓冲区大小或者调整其数据发送的调度过程等。



\begin{table}[]
  \center
  \caption{网络感知应用相关工作}
  \label{tab:related-nai-naa}
  \begin{tabular}{|m{2.2cm}|m{1.8cm}|m{4.5cm}|m{4.5cm}|}
    \hline
    \emph{研究工作}
    & \emph{协同类型}
    & \emph{协同方式}
    & \emph{主要问题}
    \\\hline
    ECN~\cite{ramakrishnan2001rfc3168} & In-band & 传输层标记拥塞情况 & 信息粒度较大，难以实现最优传输
    \\\hline
    DASH~\cite{sodagar2011mpeg} & In-band & 根据网络带宽的估计值调整比特率 & 被动统计过程导致网络状态获取不准确和不及时
    \\\hline
    BBR~\cite{cardwell2017bbr} & In-band & 通过指数方式改变发送速率进行网络状态探测 & 被动统计过程导致网络状态获取不准确和不及时
    \\\hline
    FlowDirector~\cite{cardwell2017bbr} & Out-band & 通过BGP/IGP探针获取网络状态 & 对网络本身路由协议“入侵”较大
    \\\hline
    MoWIE~\cite{zhang2020mowie} & In-band / Out-band & 结合Out-band和In-band方式向应用程序提供网络状态信息 & 对应用程序“入侵”较大，已有程序需要需要大量的修改
    \\\hline
    Sextant~\cite{zhang2021sextant} & Out-band & 基于ALTO协议获取网络状态 & 基于BGP-LS的南向协议缺乏网络性能状态获取
    \\\hline
    PAN~\cite{kruger2021api} & Programming & 提出路径可见的编程API & 仅提出应用层API，未解决数据流和路径的绑定
    \\\hline
    NCE~\cite{baniamerian2022nce} & In-band & 在ECN基础上增加应用向网络设备提供信息的协议 & 设备适配性较差，需要支持NCE协议设备
    \\\hline
  \end{tabular}
\end{table}

\textbf{基于带内（In-band）控制的网络感知应用。}基于带内控制的网络感知应用利用与数据传输相同的路径获取网络状态并调整应用策略。如ECN（Explicit Congestion Notification，ECN）~\cite{ramakrishnan2001rfc3168}是传输层中一种提供快速的拥塞通知方法。然而，ECN方法信息粒度较粗，从而限制了其效果。NCE~\cite{baniamerian2022nce}在ECN基础上增加应用向网络设备提供信息的协议，然而NCE设备适配性较差，需要支持NCE协议设备。基于DASH的算法~\cite{sodagar2011mpeg} 根据网络带宽的估计值调整比特率，基于DASH的应用程序存在一个普遍的缺点，应用程序只能通过数据平面统计数据间接“猜测”网络状态，当网络状态不稳定时，这可能会导致不准确和不及时的推断。BBR~\cite{cardwell2017bbr}通过slow-start方式开始数据流发送，并通过指数方式改变发送速率进行网络状态探测，直到收敛到最优值，也存在被动性的缺点。对于特定类型的应用程序（如视频），还有研究~\cite{nathan2019end,zhou2019learning,fouladi2018salsify} 结合应用程序级指标（例如QoE）来指导传输级别的控制，但它们都是通过被动方式获取“不可靠”网络信息。

\textbf{基于带外（Out-band）控制的网络感知应用。}基于带外控制的网络感知应用通过与数据传输不同的路径获取网络状态并调整应用策略。如Sextant~\cite{zhang2021sextant}提出了基于ALTO协议获取网络状态框架，该框架通过BGP和BGP-LS获取网络状态并通过ALTO协议提供给应用程序，然而对于如带宽和延迟等实时网络状态并未提供相应支持。FlowDirector~\cite{cardwell2017bbr}通过BGP/IGP探针获取网络状态，但FlowDirector对网络本身路由协议“入侵”较大（比如获取OSPF网络状态需要在每个OSPF area部署OSPF实例从而与网络原有OSPF实例形成对等邻居）。MoWIE~\cite{zhang2020mowie}提出了一套暴露网络状态信息的框架，通过Out-band和In-band方式向应用程序以自适应速率提供网络状态信息，然而MoWIE对应用程序“入侵”较大，已有程序需要大量的修改才能集成其功能。

\textbf{基于协同编程（Programming）的网络感知应用。}基于协同编程的网络感知应用在编程角度通过相应的API实现应用对网络的感知。如PAN~\cite{kruger2021api}提出了路径可见的应用层编程API框架，但未解决实现过程中的数据流和路径的绑定。



\begin{table}[t]
  \center
  \caption{网络和应用双向感知相关工作}
  \label{tab:related-nai-nai}
  \begin{tabular}{|m{2cm}|m{1.8cm}|m{4.5cm}|m{4.5cm}|}
    \hline
    \emph{研究工作}
    & \emph{协同类型}
    & \emph{协同方式}
    & \emph{主要问题}
    \\\hline
    DAWN~\cite{wang2020dawn} & Programming & 通过程序注释集成网络和应用编程以减少程序“入侵” & 对单套接字多数据流应用无法提供细粒度的网络控制
    \\\hline
    Flightplan~\cite{sultana2021leveraging} & Programming & 基于P4设备实现针对网络和In-network应用的协同 & 对于通用网络应用不适用
    \\\hline
    SmartTags~\cite{munir2022smarttags} & In-band & 结合应用类型（Tags）和网络事件（Events）分析其关联 & 仅提供状态分析，不提供控制功能
    \\\hline
    SARSA~\cite{gholami2022applicationspecific} & Out-band & 利用强化学习实现资源动态预留 & 对于运行时间较短的应用无法提供准确资源配置
    \\\hline
    TCN~\cite{dunefsky2022transport} & Out-band & 基于ALTO协议实现网络状态获取和传输层控制 & 针对特定网络设计
    \\\hline
  \end{tabular}
\end{table}

\subsection{网络与应用双向感知相关工作}
网络与应用双向感知（Networking-application Bidirectional Awareness, NABA）结合了AAN和NAA，旨在实现网络和应用互相感知对方状态，从而实现更加完整和灵活的网络控制和应用逻辑调整。\cref{tab:related-nai-nai}列出了当前主要的网络与应用双向感知相关工作。如DAWN~\cite{wang2020dawn}提出了通过程序注释集成网络和应用编程，使得应用程序通过简单的代码注释即可控制应用和网络，然而它对单套接字多数据流（SSMD）应用无法提供细粒度的网络控制。Flightplan~\cite{sultana2021leveraging}基于P4设备实现针对网络和In-network应用的协同，但对于本文所针对的终端设备上的应用不适用。SmartTags~\cite{munir2022smarttags}通过结合应用程序类型（Tags）和网络事件（Events）来分析其关联，以辅助未来网络与应用相互感知的应用场景，然而，SmartTags仅提供状态分析，不提供实际的控制功能。SARSA~\cite{gholami2022applicationspecific}利用强化学习实现网络和计算资源的动态预留，然而对于运行时间较短的应用无法提供准确资源配置。TCN~\cite{dunefsky2022transport}则提供了更加完整的基于ALTO~\cite{shalunov2014applicationlayer}协议的网络状态获取和传输层控制框架，但TCN针对特定网络设计，在通用性方面还有待提升。

% \textbf{网内计算。} 
% 另一个有趣且相关的主题是在网络中运行应用程序。随着网络节点的可编程性增加，应用程序可以将其部分逻辑卸载到网络中进行一些实时计算。这样，平均往返延迟和服务器上的计算量都可以大大降低。当前的研究~\cite{jin2017netcache,jin2018netchain} 利用可编程交换机，主要在交换机上实现简单的累加操作、快速键值存储等。

% \subsection{已有工作在现代网络背景下的主要问题}

\section{本章小结}
本章系统地回顾了关于网络可靠性和适应性的前沿研究，概述了控制平面验证和数据平面验证领域的最新进展，并综述了网络协同应用编程的最新技术。通过对相关工作的综合审视，为后续章节的研究工作提供了重要背景和基础。